PRISM

Benchmark
Model:repudiation_malicious v.1 (PTA)
Parameter(s)T = 20
Property:deadline (prob-reach-time-bounded)
Invocation (specific)
./fix-syntax ./prism -javamaxmem 11g -cuddmaxmem 4g -mtbdd -e 1e-6 -maxiters 1000000 repudiation_malicious.prism repudiation_malicious.props --property deadline -const T=20
Execution
Walltime:27.78049063682556s
Return code:0
Relative Error:0.0
Log
PRISM
=====

Version: 4.5.dev
Date: Sun Mar 15 03:30:04 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -mtbdd -e 1e-6 -maxiters 1000000 repudiation_malicious.prism repudiation_malicious.props --property deadline -const T=20

Parsing model file "repudiation_malicious.prism"...

Type:        PTA
Modules:     originator recipient 
Variables:   o x r y 

Parsing properties file "repudiation_malicious.props"...

2 properties:
(1) "deadline": Pmax=? [ F<T "gains_information" ]
(2) "eventually": Pmax=? [ F "gains_information" ]

---------------------------------------------------------------------

Model checking: "deadline": Pmax=? [ F<T "gains_information" ]
Property constants: T=20

Building PTA...

PTA: 2 clocks, 35 locations, 73 transitions
Target (o=10) satisfied by 5 locations.
Modifying PTA to encode time bound from property...
New PTA: 3 clocks, 36 locations, 90 transitions

Building initial STPG...

Building forwards reachability graph... 25707 states
Graph constructed in 0.659 secs.
Graph: 25707 symbolic states (1 initial, 305 target)

Model checking STPG...
STPG model checked in 1.269 secs.
23047/25707 states converged.
Diff across 1 initial state: 0.005657962875194822
Lower/upper bounds for 1 initial state: 0.1 - 0.10565796287519483
Max diff over all states: 1.0
1642 refineable states.

Refinement 1...
827 states successfully refined in 3.069 secs.
2833+0=2833 states of STPG rebuilt in 0.0 secs.
New STPG has 26534 states.

Model checking STPG...
STPG model checked in 0.939 secs.
24088/26534 states converged.
Diff across 1 initial state: 0.005657962875194822
Lower/upper bounds for 1 initial state: 0.1 - 0.10565796287519483
Max diff over all states: 1.0
1662 refineable states.

Refinement 2...
877 states successfully refined in 3.16 secs.
2483+0=2483 states of STPG rebuilt in 0.0 secs.
New STPG has 27411 states.

Model checking STPG...
STPG model checked in 0.906 secs.
25537/27411 states converged.
Diff across 1 initial state: 0.005657962875194822
Lower/upper bounds for 1 initial state: 0.1 - 0.10565796287519483
Max diff over all states: 1.0
1031 refineable states.

Refinement 3...
576 states successfully refined in 2.47 secs.
2073+0=2073 states of STPG rebuilt in 0.0 secs.
New STPG has 28059 states.

Model checking STPG...
STPG model checked in 1.033 secs.
26282/28059 states converged.
Diff across 1 initial state: 9.463503751948321E-4
Lower/upper bounds for 1 initial state: 0.1047116125 - 0.10565796287519483
Max diff over all states: 0.19509065236558698
1051 refineable states.

Refinement 4...
753 states successfully refined in 3.409 secs.
2315+0=2315 states of STPG rebuilt in 0.0 secs.
New STPG has 28986 states.

Model checking STPG...
STPG model checked in 0.979 secs.
27077/28986 states converged.
Diff across 1 initial state: 9.463503751948321E-4
Lower/upper bounds for 1 initial state: 0.1047116125 - 0.10565796287519483
Max diff over all states: 0.1056572644488625
906 refineable states.

Refinement 5...
584 states successfully refined in 2.554 secs.
1768+0=1768 states of STPG rebuilt in 0.0 secs.
New STPG has 29591 states.

Model checking STPG...
STPG model checked in 1.168 secs.
27518/29591 states converged.
Diff across 1 initial state: 9.463503751948321E-4
Lower/upper bounds for 1 initial state: 0.1047116125 - 0.10565796287519483
Max diff over all states: 0.1056572644488625
596 refineable states.

Refinement 6...
497 states successfully refined in 2.3 secs.
1565+0=1565 states of STPG rebuilt in 0.0 secs.
New STPG has 30088 states.

Model checking STPG...
STPG model checked in 1.48 secs.
27883/30088 states converged.
Diff across 1 initial state: 8.466138073370821E-7
Lower/upper bounds for 1 initial state: 0.10565711626138749 - 0.10565796287519483

Initial STPG: 25707 states (1 initial), 76866 transitions, 63657 choices, 28365 choice sets, p1max/avg = 4/1.10, p2max/avg = 5/2.24
Final STPG: 30088 states (1 initial), 103658 transitions, 82743 choices, 33260 choice sets, p1max/avg = 10/1.11, p2max/avg = 15/2.49

Terminated after 6 refinements in 26.99 secs.

Abstraction-refinement time breakdown:
* 2.21 secs (8.2%) = Building initial STPG
* 0.00 secs (0.0%) = Rebuilding STPG (6 x avg 0.00 secs)
* 7.77 secs (28.8%) = model checking STPG (7 x avg 1.11 secs) (lb=29.6%) (prob0=16.9%) (pre=91.5%) (iters=332)
* 16.96 secs (62.9%) = refinement (6 x avg 2.83 secs)

Final diff across 1 initial state: 8.466138073370821E-7
Final lower/upper bounds for 1 initial state: 0.10565711626138749 - 0.10565796287519483

Model checking completed in 27.074 secs.

Result (maximum probability): 0.10565753956829116


Overall running time: 27.581 seconds.